/LMAR=0/XLINE=3/FONT#0=BAXL30/FONT#1=BAXM30/FONT#2=BASB30/FONT#3=SUB/FONT#4=SUP/FONT#5=BASL35/FONT#6=NGR25/FONT#7=MATH30/FONT#8=FIX25/FONT#9=GRKB30



␈↓ α∧␈↓α␈↓ βpEXPRESSION OF MODALITY IN FIRST ORDER LOGIC

␈↓ α∧␈↓␈↓ αTFor␈αreasons␈αthat␈αwill␈αbe␈αexplained,␈αI␈αthink␈αartificial␈αintelligence␈αrequires␈αmodalities␈αsuch␈αas
␈↓ α∧␈↓possibility,␈α∞necessity,␈α∞knowledge,␈α∞belief,␈α
obligation␈α∞and␈α∞futurity,␈α∞but␈α∞I␈α
think␈α∞modal␈α∞logic␈α∞is␈α∞not␈α
a
␈↓ α∧␈↓good␈α
framework␈αfor␈α
expressing␈α
them.␈α The␈α
object␈αof␈α
these␈α
notes␈αis␈α
to␈α
describe␈αa␈α
way␈αof␈α
expressing
␈↓ α∧␈↓modal␈αstatements␈αin␈αordinary␈αfirst␈αorder␈αlogic.␈α In␈αthe␈αfirst␈αsection,␈αwe␈αwill␈αtranslate␈α
the␈αlanguage
␈↓ α∧␈↓of␈α
propositional␈α
modal␈α
logic␈α
into␈α
first␈α
order␈α
logic.␈α
 We␈α
will␈α
mainly␈α
be␈α
covering␈α
familiar␈α
ground;
␈↓ α∧␈↓our formulas will be somewhat longer than the corresponding formulas of modal logic.

␈↓ α∧␈↓␈↓ αTIn␈α⊃the␈α⊃second␈α⊃section,␈α⊂I␈α⊃will␈α⊃give␈α⊃an␈α⊂application␈α⊃to␈α⊃formalizing␈α⊃some␈α⊃puzzles␈α⊂involving
␈↓ α∧␈↓knowledge␈αwhich␈αI␈αdon't␈αthink␈αare␈αfeasible␈α
in␈αunadorned␈αmodal␈αlogic.␈α Anyway␈αthey␈αhaven't␈α
been
␈↓ α∧␈↓done.

␈↓ α∧␈↓␈↓ αTIn␈α∂the␈α∞third␈α∂section,␈α∂I␈α∞will␈α∂discuss␈α∂some␈α∞of␈α∂the␈α∞issues␈α∂of␈α∂formalization␈α∞of␈α∂modalities␈α∂in␈α∞a
␈↓ α∧␈↓general way.

␈↓ α∧␈↓1. Propositions and the first order theory MODAL1

␈↓ α∧␈↓␈↓ αTWe␈α
introduce␈α∞a␈α
sort␈α∞of␈α
entities␈α∞called␈α
␈↓↓propositions␈↓␈α
and␈α∞use␈α
␈↓↓P,␈↓␈α∞␈↓↓P0,␈↓␈α
␈↓↓P1,␈↓␈α∞␈↓↓P2,␈↓␈α
etc.␈α∞and␈α
␈↓↓Q,␈↓
␈↓ α∧␈↓␈↓↓Q0,␈↓␈αetc.␈αas␈αvariables␈αdenoting␈αpropositions.␈α There␈αis␈αa␈αpredicate␈αof␈αpropositions␈αcalled␈α␈↓↓true,␈↓␈αand
␈↓ α∧␈↓␈↓↓true P␈↓␈α∩is␈α∩the␈α∩assertion␈α∩that␈α∩the␈α∩proposition␈α∩␈↓↓P␈↓␈α∩is␈α∩true.␈α∩ From␈α∩propositions␈α∩we␈α∩can␈α∪get␈α∩other
␈↓ α∧␈↓propositions␈αby␈αfunctions␈αimitating␈α
the␈αBoolean␈αoperators.␈α Thus␈α
we␈αhave␈α␈↓↓not P␈↓,␈α␈↓↓P and Q␈↓,␈α
␈↓↓P or Q␈↓,
␈↓ α∧␈↓and␈α
␈↓↓P implies Q␈↓,␈α
etc.␈α Finally,␈α
we␈α
have␈αthe␈α
modal␈α
functions␈α
␈↓↓Nec P␈↓␈αand␈α
␈↓↓Poss P␈↓.␈α
 The␈αfollowing␈α
are
␈↓ α∧␈↓axioms:

␈↓ α∧␈↓1)␈↓ αt ␈↓↓∀P.(true Not P ≡ ¬true P)␈↓,

␈↓ α∧␈↓2)␈↓ αt ␈↓↓∀P Q.(true (P and Q) ≡ true P ∧ true Q)␈↓,

␈↓ α∧␈↓3)␈↓ αt ␈↓↓∀P Q.(true (P or Q) ≡ true P ∨ true Q)␈↓,

␈↓ α∧␈↓and

␈↓ α∧␈↓4)␈↓ αt ␈↓↓∀P Q.(true (P implies Q) ≡ true P ⊃ true Q)␈↓,

␈↓ α∧␈↓etc., for any additional Boolean operators that may be wanted.

␈↓ α∧␈↓␈↓ αTSo␈α⊃far␈α⊃not␈α⊃much␈α⊃has␈α⊃happened,␈α⊃because␈α⊃we␈α⊃haven't␈α⊃done␈α⊃anything␈α⊃with␈α⊃our␈α⊃imitation
␈↓ α∧␈↓Boolean␈α
operators␈α∞that␈α
couldn't␈α∞be␈α
done␈α
without␈α∞them.␈α
 Indeed␈α∞if␈α
we␈α
were␈α∞to␈α
use␈α∞the␈α
systematic
␈↓ α∧␈↓notational convention

␈↓ α∧␈↓␈↓ αT␈↓↓p = true P␈↓,

␈↓ α∧␈↓then␈α⊂any␈α⊃formula␈α⊂involving␈α⊃␈↓↓true␈↓␈α⊂applied␈α⊃to␈α⊂some␈α⊃combination␈α⊂of␈α⊃proposition␈α⊂letters␈α⊃with␈α⊂the
␈↓ α∧␈↓imitation␈α
Boolean␈α
operators␈α
could␈α
be␈α
rewritten␈α
in␈α
terms␈α
of␈α
the␈α
␈↓↓p␈↓'s␈α
and␈α
ordinary␈α
Boolean␈α
operators.
␈↓ α∧␈↓We get something new when we introduce the axioms satisfied by the modal operators

␈↓ α∧␈↓5)␈↓ αt ␈↓↓∀P.(true Nec P ⊃ true P)␈↓,

␈↓ α∧␈↓␈↓ ε|1␈↓ ∧



␈↓ α∧␈↓6)␈↓ αt ␈↓↓∀P Q.(true (Nec P and Nec Q) ⊃ true Nec(P and Q))␈↓,

␈↓ α∧␈↓and

␈↓ α∧␈↓7)␈↓ αt ␈↓↓VP Q.(true Nec P ∧ true Nec(P implies Q) ⊃ true Nec Q)␈↓

␈↓ α∧␈↓together␈α
with␈α∞the␈α
necessity␈α∞of␈α
your␈α∞favorite␈α
set␈α∞of␈α
axioms␈α∞for␈α
the␈α∞propositional␈α
calculus,␈α∞e.g.␈α
the
␈↓ α∧␈↓formulas

␈↓ α∧␈↓8)␈↓ αt ␈↓↓∀P.Nec((P or P) implies P)␈↓,

␈↓ α∧␈↓9)␈↓ αt ␈↓↓∀P Q.Nec(Q implies (P or Q))␈↓,

␈↓ α∧␈↓10)␈↓ αt ␈↓↓∀P Q.Nec((P or Q) implies (Q or P))␈↓,

␈↓ α∧␈↓and

␈↓ α∧␈↓11)␈↓ αt ␈↓↓∀P Q R.Nec((Q implies R) implies ((P or Q) implies (P or R)))␈↓,

␈↓ α∧␈↓which␈αwe␈αhave␈αcopied␈αfrom␈α(Hughes␈αand␈αCresswell␈α1968)␈αwho␈αcopied␈αthem␈αfrom␈αWhitehead␈αand
␈↓ α∧␈↓Russell's ␈↓↓Principia Mathematica␈↓.

␈↓ α∧␈↓We also have

␈↓ α∧␈↓12)␈↓ αt ␈↓↓∀P.(true Poss P ≡ true Not Nec Not P)␈↓.

␈↓ α∧␈↓␈↓ αTWith␈α
just␈αthese␈α
axioms,␈αwe␈α
have␈α
a␈αsystem␈α
equivalent␈αto␈α
M␈α
in␈αthe␈α
sense␈αthat␈α
a␈α
sentence␈αof
␈↓ α∧␈↓MODAL1␈α
can␈α
be␈α
proved␈α
if␈α
and␈α
only␈α
if␈α
the␈α
corresponding␈α
sentence␈α
of␈α
M␈α
can␈α
be␈α
proved.␈α
 S4␈αis
␈↓ α∧␈↓given by adjoining to the above axioms

␈↓ α∧␈↓13)␈↓ αt ␈↓↓∀P.(true Nec P ⊃ true Nec Nec P␈↓,

␈↓ α∧␈↓and S5 is given by adjoining

␈↓ α∧␈↓14)␈↓ αt ␈↓↓∀P.(true Poss P ⊃ true Nec Poss P)␈↓.

␈↓ α∧␈↓2. Kripke Semantics

␈↓ α∧␈↓␈↓ αTWe␈αget␈αthe␈αKripke␈αsemantics␈αby␈αintroducing␈α
another␈αsort␈αcalled␈αpossible␈αworlds,␈αand␈αwe␈α
use
␈↓ α∧␈↓variables␈α
␈↓↓w,␈↓␈α
␈↓↓w0,␈↓␈α
␈↓↓w1,␈↓␈α
etc.␈α∞for␈α
them.␈α
 We␈α
have␈α
a␈α
relation␈α∞␈↓↓a(w1,w2)␈↓␈α
saying␈α
that␈α
the␈α
world␈α∞␈↓↓w2␈↓␈α
is
␈↓ α∧␈↓possible␈α∞(or␈α∂accessible)␈α∞from␈α∂the␈α∞world␈α∂␈↓↓w1.␈↓␈α∞We␈α∂extend␈α∞the␈α∂predicate␈α∞␈↓↓true␈↓␈α∂to␈α∞take␈α∂a␈α∞world␈α∂as␈α∞a
␈↓ α∧␈↓second␈αargument␈αso␈αthat␈αwe␈αhave␈α␈↓↓true(P,w),␈↓␈αand␈αwe␈αintroduce␈αa␈αpreferred␈αworld␈αcalled␈α␈↓↓RW␈↓␈α(the
␈↓ α∧␈↓real␈αworld)␈αand␈α
identify␈α␈↓↓true P␈↓␈αand␈α
␈↓↓true(P,RW).␈↓␈αThe␈αpropositional␈α
axioms␈αare␈αextended␈α
in␈αthe
␈↓ α∧␈↓obvious way so that we have such axioms as

␈↓ α∧␈↓15)␈↓ αt ␈↓↓∀P Q w.(true(P and Q,w) ≡ true(P,w) ∧ true(Q,w))␈↓

␈↓ α∧␈↓analogous to (2) and similar axioms analogous to the others.

␈↓ α∧␈↓␈↓ ε|2␈↓ ∧



␈↓ α∧␈↓␈↓ αTThe truth of the modal functions Nec and Poss is determined by the axioms

␈↓ α∧␈↓16)␈↓ αt ␈↓↓∀P w.(true(Nec P,w) ≡ ∀w1.(a(w,w1) ⊃ true(P,w1))␈↓

␈↓ α∧␈↓and

␈↓ α∧␈↓17)␈↓ αt ␈↓↓∀P w.(true(Poss P,w) ≡ ∃w1.(a(w,w1) ∧ true(P,w1))␈↓.

␈↓ α∧␈↓␈↓ αTThe reflexivity of ␈↓↓a␈↓ as expressed by

␈↓ α∧␈↓18)␈↓ αt ␈↓↓∀w.a(w,w)␈↓

␈↓ α∧␈↓is equivalent to (5).  S4 is obtained by making ␈↓↓a␈↓ transitive, i.e.

␈↓ α∧␈↓19)␈↓ αt ␈↓↓∀w1 w2 w3.(a(w1,w2) ∧ a(w2,w3) ⊃ a(w1,w3))␈↓,

␈↓ α∧␈↓and S5 is obtained by adjoining

␈↓ α∧␈↓20)␈↓ αt ␈↓↓∀w1 w2.(a(w1,w2) ⊃ a(w2,w1))␈↓

␈↓ α∧␈↓so as to make ␈↓↓a␈↓ an equivalence relation.

␈↓ α∧␈↓␈↓ αTThe␈αadvantages␈αand␈αdisadvantages␈αof␈αthe␈αpredicate␈αcalculus␈αtreatment␈αover␈αthe␈αmodal␈αlogic
␈↓ α∧␈↓treatment␈αseem␈αso␈αfar␈αto␈αbe␈αa␈αmatter␈αof␈αtaste.␈α The␈αtraditional␈αtreatment␈αmodifies␈αthe␈αlogic␈αwhich
␈↓ α∧␈↓is␈α∪a␈α∪nuisance␈α∩for␈α∪people␈α∪who␈α∩experiment␈α∪with␈α∪predicate␈α∩calculus␈α∪theorem␈α∪provers␈α∪or␈α∩proof
␈↓ α∧␈↓checkers.␈α∂ On␈α∂the␈α∂other␈α∞hand,␈α∂one␈α∂may␈α∂feel␈α∂that␈α∞quantifiers␈α∂are␈α∂more␈α∂complicated␈α∂than␈α∞modal
␈↓ α∧␈↓operators.␈α∩ Treating␈α∩quantified␈α∩modal␈α∩logic␈α∩might␈α∩give␈α∩more␈α∩information␈α∩about␈α∩whether␈α⊃the
␈↓ α∧␈↓predicate␈αcalculus␈αtreatment␈αis␈αpreferable,␈αbut␈αwe␈αhaven't␈αtried␈αthat␈αyet.␈α Instead␈αwe␈αhave␈αworked
␈↓ α∧␈↓on␈α
formulating␈α
some␈α
puzzles␈α
in␈αthe␈α
logic␈α
of␈α
knowledge.␈α
 There␈αwe␈α
know␈α
how␈α
to␈α
do␈α
some␈αthings
␈↓ α∧␈↓that␈αare␈αrequired␈αfor␈αsolving␈αthe␈αpuzzles␈αin␈αthe␈αpredicate␈αcalculus␈αtreatment␈αusing␈αpossible␈α
worlds,
␈↓ α∧␈↓and we don't yet know how to do them in modal logic.

␈↓ α∧␈↓3. Knowledge as a modal operator

␈↓ α∧␈↓␈↓ αTMany␈α∩philosophical␈α∩authors␈α∩have␈α∩treated␈α∩knowledge␈α∩using␈α∩modal␈α∩operators.␈α∩ (Hintikka
␈↓ α∧␈↓1962)␈α∞is␈α∞a␈α∞major␈α∞reference␈α∞and␈α∞the␈α∂Kripke␈α∞semantics␈α∞of␈α∞modal␈α∞logic␈α∞is␈α∞extensively␈α∂discussed␈α∞in
␈↓ α∧␈↓Sato's␈α(1977)␈α
thesis.␈α The␈α
main␈αformal␈α
emphasis␈αhas␈α
been␈αon␈α
"knowing␈αthat"␈α
where␈αthe␈αoperand␈α
is
␈↓ α∧␈↓a␈α∩sentence␈α∩or␈α∩proposition,␈α∩and␈α∩the␈α⊃literary␈α∩philosophers␈α∩have␈α∩emphasized␈α∩the␈α∩importance␈α⊃of
␈↓ α∧␈↓"knowing␈α
how",␈α
although␈α
it␈α
hasn't␈α
been␈α
treated␈α∞formally.␈α
 In␈α
order␈α
to␈α
solve␈α
the␈α
puzzles␈α∞we␈α
shall
␈↓ α∧␈↓discuss␈α⊂in␈α⊂this␈α⊂section,␈α⊃it␈α⊂is␈α⊂important␈α⊂to␈α⊂emphasize␈α⊃"knowing␈α⊂what",␈α⊂e.g.␈α⊂ ␈↓↓"Pat␈α⊃knows␈α⊂Mike's
␈↓ α∧␈↓↓telephone number"␈↓ or ␈↓↓"The second wiseman doesn't know the color of his spot"␈↓.

␈↓ α∧␈↓␈↓ αTWe␈α↔shall␈α↔emphasize␈α↔semantic␈α↔treatments␈α↔and␈α↔introduce␈α↔an␈α↔new␈α↔accessibilty␈α↔relation
␈↓ α∧␈↓␈↓↓A(w1,w2,person,time)␈↓␈α∂which␈α∂means␈α∞that␈α∂world␈α∂␈↓↓w2␈↓␈α∞is␈α∂accessible␈α∂(possible)␈α∞from␈α∂world␈α∂␈↓↓w1␈↓␈α∞form
␈↓ α∧␈↓person␈α⊃␈↓↓person␈↓␈α⊃at␈α⊃time␈α⊃␈↓↓time.␈↓␈α⊃We␈α⊃introduce␈α⊃time,␈α⊃because␈α⊃our␈α⊃puzzles␈α⊃involve␈α∩people␈α⊃learning
␈↓ α∧␈↓things.

␈↓ α∧␈↓(to be continued)

␈↓ α∧␈↓␈↓ ε|3␈↓ ∧



␈↓ α∧␈↓John McCarthy
␈↓ α∧␈↓Artificial Intelligence Laboratory
␈↓ α∧␈↓Computer Science Department
␈↓ α∧␈↓Stanford University
␈↓ α∧␈↓Stanford, California 94305

␈↓ α∧␈↓ARPANET: MCCARTHY@SU-AI

␈↓ α∧␈↓␈↓εThis draft of MODAL[S78,JMC] PUBbed at 15:49 on June 29, 1978.␈↓








































␈↓ α∧␈↓␈↓ ε|4␈↓ ∧